Library cross_sum

Require Export PointsType.
Require Import incidence.
Require Import cross_point.
Require Import isogonal_conjugate.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition cross_sum P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  cTriple (q×w + r×v) (r×u + p×w) (p×v + q×u)
 end.

Definition is_cross_sum P Q R := eq_points P (cross_sum Q R).

Lemma cross_sum_property :
 ∀ P U,
  is_not_on_sidelines P →
  is_not_on_sidelines U →
  eq_points (cross_sum P U) (cross_point (isogonal_conjugate P) (isogonal_conjugate U)).
Proof.
intros P U.
destruct P.
destruct U.
unfold eq_points, is_not_on_sidelines, trilinear_pole, isogonal_conjugate.
simpl in ×.
split;
field;intuition.
Qed.

End Triangle.